(declare-fun a () (_ BitVec 8))
(declare-fun b () (_ BitVec 8))
(declare-fun c () (_ BitVec 8))
(declare-fun d () (_ BitVec 8))
(declare-fun e () (_ BitVec 8))
(declare-fun f () (_ BitVec 8))
(declare-fun j () (_ BitVec 8))
(declare-fun g () (_ BitVec 8))
(declare-fun h () (_ BitVec 8))
(assert (bvuge (bvlshr ((_ zero_extend 24) h) ((_ zero_extend 24) (_ bv2 8))) (_ bv8 32)))
(assert (distinct ((_ zero_extend 24) g) (_ bv0 32)))
(assert (let ((?d ((_ zero_extend 24) b))(?j ((_ zero_extend 24) c))(?i ((_ zero_extend 24) j))(?l ((_ zero_extend 24) g))(?aa ((_ zero_extend 24) h))) (bvult (bvadd (_ bv616 32) (bvmul (_ bv4294967295 32) (bvadd ?aa ?l ?i ?j ?d (_ bv9 32)))) (_ bv256 32))))
(assert (let ((?am ((_ zero_extend 24) a))(?j ((_ zero_extend 24) c))(?an ((_ zero_extend 24) d))(?ao ((_ zero_extend 24) e))(?ap ((_ zero_extend 24) f))) (distinct (bvadd ?ap ?ao ?an ?j ?am) (_ bv0 32))))
(check-sat)
